(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


(** ** Matrix Module *)

Require Export Matrix.MMat.MMat_def.
Require Export Matrix.MMat.Mlist_function.
Require Export Matrix.MMat.MMat_add.
Require Export Matrix.MMat.MMat_trans.
Require Export Matrix.MMat.MMat_mult.
Require Export Matrix.Mat.Matrix_Module.
Require Export Setoid.
Require Export Relation_Definitions.
Set Implicit Arguments.

(* ################################################################# *)
(** * Definition of Module Type *)

Module Type MMType.

Parameter A :Set.
Parameter Zero One : A.
Parameter opp : A -> A.
Parameter add sub mul: A->A->A.

Infix " + " := add.
Infix " - " := sub.
Infix " * " := mul.

Parameter add_comm : forall x y , x + y = y + x.
Parameter add_assoc : forall x y z , x + y + z = x + (y + z).
Parameter add_assoc2 : forall x y z w, (x+y)+(z+w) = (x+z)+(y+w).
Parameter add_zero_l : forall x , Zero + x  = x.
Parameter add_zero_r : forall x , x + Zero = x.

Parameter sub_assoc : forall x y z, x - y - z = x - (y + z).
Parameter sub_assoc2: forall x y z w, (x+y)-(z+w) = (x-z)+(y-w).
Parameter sub_opp : forall x y , x - y = opp (y - x ).
Parameter sub_zero_l:forall x ,Zero - x = opp x.
Parameter sub_zero_r:forall x , x - Zero = x.
Parameter sub_self : forall x , x-x =Zero.

(*Parameter mul_one_l : forall x , One * x = x. *)
Parameter mul_add_distr_l : forall x y z, (x+y)*z = x*z + y*z.
Parameter mul_add_distr_r : forall x y z, x*(y+z) = x*y + x*z.
Parameter mul_sub_distr_l : forall x y z, (x-y)*z = x*z - y*z.
Parameter mul_sub_distr_r : forall x y z, x*(y-z) = x*y - x*z.
Parameter mul_assoc : forall x y z, x * y * z = x * (y * z).
Parameter mul_zero_l : forall x , Zero * x = Zero.
Parameter mul_zero_r : forall x , x * Zero = Zero.
Parameter mul_one_l : forall x , One * x = x.
Parameter mul_comm : forall x y, x*y = y*x.

End MMType.

(** * Definition of Matrix Module *)

Module Type Size.
Parameter m n p k :nat.
End Size.

Module MMatrix (M : MMType).
(*
Definition m := S.m.

Definition n := S.n.

Definition p := S.p.

Definition k := S.k.
*)
Definition MMO m n := @MO (Mat M.A m n) (@MO M.A M.Zero m n).

Definition MMI := @MI M.A M.Zero M.One.

Definition MMeq :=@MM_eq M.A.
Arguments MMeq {m}{n}{m2}{n2}.

Definition MMopp m0 n0 := @matrix_map (Mat M.A m0 n0) (matrix_map M.A M.opp).
Arguments MMopp {m0}{n0}{m}{n}.

Definition MMadd m0 n0 := @matrix_each (@Mat M.A m0 n0) (@matrix_each M.A M.add m0 n0).
Arguments MMadd {m0}{n0}{m}{n}.
(*
Definition MMaddnm m n := @matrix_each (@Mat M.A n m) (@matrix_each M.A M.add n m).
Arguments MMaddnm {m0} {n0}.

Definition MMaddmp := @matrix_each (@Mat M.A m p) (@matrix_each M.A M.add m p).
Arguments MMaddmp {m0} {n}.

Definition MMaddnp := @matrix_each (@Mat M.A n p) (@matrix_each M.A M.add n p).
Arguments MMaddnp {m} {n0}.
*)
Definition MMsub m0 n0 := @matrix_each (@Mat M.A m0 n0) (@matrix_each M.A M.sub m0 n0).
Arguments MMsub {m0}{n0}{m}{n}.
(*
Definition MMsubnm := @matrix_each (@Mat M.A n m) (@matrix_each M.A M.sub n m).
Arguments MMsubnm {m0} {n0}.

Definition MMsubmp := @matrix_each (@Mat M.A m p) (@matrix_each M.A M.sub m p).
Arguments MMsubmp {m0} {n}.
*)
Definition MMtrans m0 n0 := @mmtrans M.A M.Zero m0 n0.
Arguments MMtrans {m0}{n0}{m2}{n2}.

Definition MMmult  :=@mmatrix_mul M.A M.Zero M.add M.mul .
Arguments MMmult {m}{n}{p}{m2} {n2} {p2}.
(*
Definition MMmultnpk:=@mmatrix_mul M.A M.Zero M.add M.mul n p k.
Arguments MMmultnpk {m2} {n2} {p2}.
*)
Notation "m1 MM+ m2" := (MMadd m1 m2) (at level 65).

Notation "m1 MM- m2" := (MMsub m1 m2) (at level 65).

Notation " MM- m" := (MMopp m) (at level 65).

Notation "m1 MM* m2" := (MMmult m1 m2) (at level 60).

Notation "MT( m )" := (MMtrans m) (at level 55).


Lemma MMeq_ref : forall {m n m2 n2:nat}, reflexive _ (@MMeq m n m2 n2).
intros. unfold reflexive. apply MM_eq_ref.
Qed.

Lemma MMeq_sym : forall {m n m2 n2:nat}, symmetric _ (@MMeq m n m2 n2).
intros. unfold symmetric. apply MM_eq_sym.
Qed.

Lemma MMeq_trans : forall {m n m2 n2:nat}, transitive _ (@MMeq m n m2 n2).
intros. unfold transitive. apply MM_eq_trans.
Qed.

Add Parametric Relation {m n m2 n2:nat} : (Mat (Mat M.A m n)m2 n2) (@MMeq m n m2 n2) 
  reflexivity proved by (@MMeq_ref m n m2 n2)
  symmetry proved by (@MMeq_sym m n m2 n2)
  transitivity proved by (@MMeq_trans m n m2 n2)
  as MMeq_rel.


Notation "m1 MM= m2" := (MMeq m1 m2) (at level 70).

Lemma MMadd_comm : forall {m n m2 n2}
 (ma mb:@Mat (@Mat M.A m n) m2 n2) ,
  ma MM+ mb MM=  mb MM+ ma.
Proof.
  intros.
  apply mmatrix_each_comm with(Zero:=M.Zero).
  apply M.add_zero_r. apply M.add_comm.
Qed.

(** ** A + B + C = A + ( B + C) *)

Lemma MMadd_assoc : forall {m n m2 n2}
  (ma mb mc:@Mat (@Mat M.A m n) m2 n2) , 
  (ma MM+ mb) MM+ mc MM=
  ma MM+ (mb MM+ mc).
Proof. intros. apply mmatrix_assoc with(Zero:=M.Zero).
  apply M.add_zero_r. apply M.add_assoc.
Qed.

(** ** O + A = A *)

Lemma MMadd_zero_l : forall {m n m2 n2} (ma:@Mat (@Mat M.A m n) m2 n2) , 
  ((MMO m n m2 n2) MM+ ma) MM= ma.
Proof.
  intros.
  apply mmatrix_add_zero_l.
  apply M.add_zero_r. apply M.add_zero_l.
Qed.

(** ** A + O = A *)

Lemma MMadd_zero_r : forall {m n m2 n2} (ma:Mat (Mat M.A m n) m2 n2) , 
  (ma MM+ (MMO m n m2 n2)) MM=  ma.
Proof.
  intros.
  apply mmatrix_add_zero_r.
  apply M.add_zero_r.
Qed.

(** ** A - B = - ( B - A ) *)

Lemma MMsub_opp : forall {m n m2 n2} (m1 m2:Mat (Mat M.A m n) m2 n2) , 
  m1 MM- m2 MM= MMopp (m2 MM- m1).
Proof.
  intros.
  apply mmatrix_sub_opp with(Zero:=M.Zero).
  auto. apply M.sub_zero_r. apply M.sub_opp.
Qed.

(** ** A - B - C = A - ( B + C ) *)

Lemma MMsub_assoc : forall {m n m2 n2}(ma mb mc:@Mat (Mat M.A m n) m2 n2) , 
  (ma MM- mb) MM- mc MM=
  ma MM- (mb MM+ mc).
Proof.
  intros.
  apply mmatrix_sub_assoc with(Zero:=M.Zero).
  apply M.add_zero_r. apply M.sub_zero_r. apply M.sub_assoc.
Qed.

(** ** O - A = - A *)

Lemma MMsub_zero_l : forall {m n m2 n2}(m1 :@Mat (Mat M.A m n) m2 n2),
  (MMO m n m2 n2) MM- m1 MM= MMopp m1.
Proof.
  intros.
  apply mmatrix_sub_zero_l.
  apply M.sub_zero_r. apply M.sub_zero_l.
Qed.

(** ** A - O = A *)

Lemma MMsub_zero_r:forall {m n m2 n2} (m1 :@Mat (Mat M.A m n) m2 n2),
  m1 MM- (MMO m n m2 n2) MM= m1.
Proof.
  intros.
  apply mmatrix_sub_zero_r.
  apply M.sub_zero_r.
Qed.

(** ** A - A = O *)

Lemma MMsub_self : forall {m n m2 n2} (m1:@Mat (Mat M.A m n) m2 n2),
  m1 MM- m1 MM= MMO m n m2 n2 .
Proof.
  intros.
  apply mmatrix_sub_self.
  apply M.sub_zero_r. apply M.sub_self.
Qed.


(** ** ( A + B ) * C = A * C + B * C *)

Lemma MMmul_add_distr_l : forall {m n p m2 n2 p2}
  (ma mb :Mat (Mat M.A m n) m2 n2) (mc :Mat (Mat M.A n p) n2 p2),
  (ma MM+ mb) MM* mc MM= MMadd (ma MM* mc) (mb MM* mc).
Proof.
  intros. apply mmatrix_mul_distr_l.
  apply M.add_zero_r. apply M.add_assoc2.
  apply M.mul_add_distr_l. apply M.mul_comm.
  apply M.add_zero_l. apply M.add_zero_r. intros. symmetry.
  apply M.add_assoc.
Qed.

(** ** A * ( B + C ) = A * B + A * C *)
Lemma MMmul_add_distr_r : forall {m n p m2 n2 p2}
  (ma :Mat (Mat M.A m n) m2 n2) (mb mc :Mat (Mat M.A n p) n2 p2),
  ma MM*(MMadd mb mc) MM= MMadd (ma MM* mb) (ma MM* mc).
Proof.
  intros. apply mmatrix_mul_distr_r.
  apply M.add_zero_r. apply M.add_assoc2.
  apply M.mul_add_distr_r. apply M.mul_comm.
  apply M.add_zero_l. apply M.add_zero_r. intros. symmetry.
  apply M.add_assoc.
Qed.

(** ** ( A - B ) * C = A * C - B * C *)

Lemma MMmul_sub_distr_l : forall {m n p m2 n2 p2}
  (ma mb :Mat (Mat M.A m n) m2 n2) (mc :Mat (Mat M.A n p) n2 p2),
  (ma MM- mb) MM* mc MM= MMsub (ma MM* mc) (mb MM* mc).
Proof.
  intros. apply mmatrix_mul_distr_l.
  apply M.sub_zero_r. apply M.sub_assoc2.
  apply M.mul_sub_distr_l. apply M.mul_comm.
  apply M.add_zero_l. apply M.add_zero_r.
  intros. symmetry. apply M.add_assoc.
Qed.

Lemma MMmul_sub_distr_r: forall{m n p m2 n2 p2}
  (ma :Mat (Mat M.A m n) m2 n2) (mb mc :Mat (Mat M.A n p) n2 p2),
  ma MM*(MMsub mb mc) MM= MMsub (ma MM* mb) (ma MM* mc).
Proof.
  intros. apply mmatrix_mul_distr_r.
  apply M.sub_zero_r. apply M.sub_assoc2.
  apply M.mul_sub_distr_r. apply M.mul_comm.
  apply M.add_zero_l. apply M.add_zero_r. intros. symmetry.
  apply M.add_assoc.
Qed.

Lemma MMmul_assoc : forall {m n p k m2 n2 p2 k2}
  (ma:Mat (Mat M.A m n) m2 n2) (mb :Mat (Mat M.A n p) n2 p2)
  (mc :Mat (Mat M.A p k) p2 k2),
  ma MM* mb MM* mc MM= ma MM* (mb MM* mc).
Proof.
  intros. apply mmatrix_mul_assoc. apply M.add_zero_l.
  apply M.add_zero_r. symmetry. apply M.add_assoc.
  apply M.mul_zero_r. apply M.mul_zero_l.
  apply M.mul_comm. apply M.mul_assoc.
  apply M.mul_add_distr_r. intros. apply M.mul_add_distr_l.
  apply M.add_assoc2.
Qed.

Lemma MMmul_zero_l: forall {m n p m2 n2 p2} (ma: Mat(Mat M.A n p) n2 p2),
  (MMO m n m2 n2) MM* ma MM= MMO m p m2 p2.
Proof.
  intros. apply mmatrix_mul_zero_l. apply M.mul_zero_l.
  apply M.add_zero_l. apply M.add_zero_r.
  apply M.mul_comm. symmetry. apply M.add_assoc.
Qed.

Lemma MMmul_zero_r: forall  {m n p m2 n2 p2} (ma: Mat(Mat M.A m n) m2 n2),
  ma  MM* (MMO n p n2 p2)  MM= MMO m p m2 p2.
Proof.
  intros. apply mmatrix_mul_zero_r. apply M.mul_zero_r.
  apply M.add_zero_l. apply M.add_zero_r. apply M.mul_comm.
  symmetry. apply M.add_assoc.
Qed.

Lemma MMtteq: forall { m n m2 n2 } (ma : Mat(Mat M.A m n) m2 n2),
  MMtrans (MMtrans ma) MM= ma.
Proof.
  intros. apply mmtrans_same.
Qed.

Lemma MMtrans_add: forall { m n m2 n2 } (ma mb : Mat(Mat M.A m n) m2 n2),
  MT(ma MM+ mb) MM= MT(ma) MM+ MT(mb).
Proof.
  intros. apply mmteq_f. apply M.add_zero_r.
Qed.

Lemma MMtrans_sub: forall {m n m2 n2 }  (ma mb : Mat(Mat M.A m n) m2 n2),
  MT(ma MM- mb) MM= MT(ma) MM- MT(mb).
Proof.
  intros. apply mmteq_f. apply M.sub_zero_r.
Qed.

Lemma MMtrans_mul:forall {m n p m2 n2 p2} (ma:Mat (Mat M.A m n) m2 n2)
  (mb: Mat(Mat M.A n p) n2 p2),
  MT(ma MM* mb) MM= MT(mb) MM* MT(ma).
Proof.
  intros. apply mmtrans_mul. apply M.add_zero_l.
  apply M.add_zero_r. apply M.mul_comm. symmetry.
  apply M.add_assoc.
Qed.
  

End MMatrix.

